Introduce a Hoare triple framework for Turing machines:

- TapePred: predicates on (input, work, output) tape configurations
- HoareTime: time-bounded Hoare triple {pre} tm {post} [≤ bound]
- Hoare: unbounded variant for pure correctness
- Structural rules: consequence, weakening, strengthening, monotonicity

Composition rules for all combinators:
- seqTM_hoareTime: sequential composition with intermediate predicate
- complementTM_hoareTime: output bit flipping with head bound
- ifTM_hoareTime: conditional branching with AllTapesWF tracking
- loopTM_hoareTime: loop invariant rule with variant-based termination

AllTapesWF tracks well-formedness (cell 0 = ▷, cells ≥ 1 ≠ ▷) as a
stability invariant preserved through tape transitions.

…suppression

- Extract `transitionTape`/`transitionInput` and their property lemmas
  (`_cells`, `_head_ge`, `_head_bound`) into Generic.lean as the single
  source of truth. These were previously duplicated as
  `seqTransitionTape`, `ifTransitionTape`, and `loopTransitionTape`.
- Remove `set_option linter.unusedSimpArgs false` from Hoare.lean (the
  underlying simp calls were already clean).
- Rename `AllTapesWF.ifTransition` → `AllTapesWF.transition` since the
  property is combinator-agnostic.

Net: -64 lines, zero duplication of the phase-transition tape operations.

… and TM building blocks

Extract general-purpose infrastructure from the UTM development:

**Encoding.lean**: State normalization and binary encoding primitives.
- `TM.normalize`: convert any TM to use `Fin (Fintype.card Q)` states,
  with full behavioral equivalence (`normalize_decidesInTime`)
- `Γ.encode`/`Γ.decode`, `Γw.encode`, `Dir3.encode`: 2-bit symbol/direction
  encodings with roundtrip correctness
- `Nat.toBits`/`Nat.fromBits`: fixed-width big-endian binary
- `allΓ`, `allΓFuncs`: canonical enumeration of tape symbols

**Subroutines.lean**: Five composable TM building blocks.
- `writeTM sym`: write symbol to output cell 1 and halt
- `rewindWorkTM idx`: rewind work tape to cell 1
- `scanRightTM idx`: scan work tape right until blank
- `copyInputToWorkTM idx`: copy input tape to work tape
- `compareWorkTapesTM i j`: compare two work tapes cell by cell

**Subroutines/Internal.lean**: HoareTime specifications.
- `writeTM_hoareTime`: time B+3, postcondition output cell 1 = sym.toΓ
- `rewindWorkTM_hoareTime`: time B+2, postcondition head = 1
- `rewindWorkTM_rich_hoareTime`: preserves arbitrary predicate P through rewind

**Generic.lean additions**: Frame rules for composition.
- `transitionTape_id`: transitionTape is identity when tape reads non-▷
- `transitionInput_id`: same for input tape
- `rightOfStart_allIdle` made public (needed by subroutines)

- Add time-bound formulas and tape transition explanation to Hoare.lean
  module docstring
- Add docstrings to all config wrapping functions (phase1Wrap, phase2Wrap,
  ifTestWrap, ifThenWrap, ifElseWrap, loopBodyWrap, loopTestWrap)